YES 3.3240000000000003 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ CR

mainModule Main
  (((<=) :: Ord a => a  ->  a  ->  Bool) :: Ord a => a  ->  a  ->  Bool)

module Main where
  import qualified Prelude



Case Reductions:
The following Case expression
case compare x y of
 EQ → o
 LT → LT
 GT → GT

is transformed to
primCompAux0 o EQ = o
primCompAux0 o LT = LT
primCompAux0 o GT = GT



↳ HASKELL
  ↳ CR
HASKELL
      ↳ IFR

mainModule Main
  (((<=) :: Ord a => a  ->  a  ->  Bool) :: Ord a => a  ->  a  ->  Bool)

module Main where
  import qualified Prelude



If Reductions:
The following If expression
if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to
primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0 x y False = Zero

The following If expression
if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x

is transformed to
primModNatS0 x y True = primModNatS (primMinusNatS x y) (Succ y)
primModNatS0 x y False = Succ x



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
HASKELL
          ↳ BR

mainModule Main
  (((<=) :: Ord a => a  ->  a  ->  Bool) :: Ord a => a  ->  a  ->  Bool)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
HASKELL
              ↳ COR

mainModule Main
  (((<=) :: Ord a => a  ->  a  ->  Bool) :: Ord a => a  ->  a  ->  Bool)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
compare x y
 | x == y
 = EQ
 | x <= y
 = LT
 | otherwise
 = GT

is transformed to
compare x y = compare3 x y

compare1 x y True = LT
compare1 x y False = compare0 x y otherwise

compare0 x y True = GT

compare2 x y True = EQ
compare2 x y False = compare1 x y (x <= y)

compare3 x y = compare2 x y (x == y)

The following Function with conditions
gcd' x 0 = x
gcd' x y = gcd' y (x `rem` y)

is transformed to
gcd' x zx = gcd'2 x zx
gcd' x y = gcd'0 x y

gcd'0 x y = gcd' y (x `rem` y)

gcd'1 True x zx = x
gcd'1 zy zz vuu = gcd'0 zz vuu

gcd'2 x zx = gcd'1 (zx == 0) x zx
gcd'2 vuv vuw = gcd'0 vuv vuw

The following Function with conditions
gcd 0 0 = error []
gcd x y = 
gcd' (abs x) (abs y)
where 
gcd' x 0 = x
gcd' x y = gcd' y (x `rem` y)

is transformed to
gcd vux vuy = gcd3 vux vuy
gcd x y = gcd0 x y

gcd0 x y = 
gcd' (abs x) (abs y)
where 
gcd' x zx = gcd'2 x zx
gcd' x y = gcd'0 x y
gcd'0 x y = gcd' y (x `rem` y)
gcd'1 True x zx = x
gcd'1 zy zz vuu = gcd'0 zz vuu
gcd'2 x zx = gcd'1 (zx == 0) x zx
gcd'2 vuv vuw = gcd'0 vuv vuw

gcd1 True vux vuy = error []
gcd1 vuz vvu vvv = gcd0 vvu vvv

gcd2 True vux vuy = gcd1 (vuy == 0) vux vuy
gcd2 vvw vvx vvy = gcd0 vvx vvy

gcd3 vux vuy = gcd2 (vux == 0) vux vuy
gcd3 vvz vwu = gcd0 vvz vwu

The following Function with conditions
absReal x
 | x >= 0
 = x
 | otherwise
 = `negate` x

is transformed to
absReal x = absReal2 x

absReal1 x True = x
absReal1 x False = absReal0 x otherwise

absReal0 x True = `negate` x

absReal2 x = absReal1 x (x >= 0)

The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
reduce x y
 | y == 0
 = error []
 | otherwise
 = x `quot` d :% (y `quot` d)
where 
d  = gcd x y

is transformed to
reduce x y = reduce2 x y

reduce2 x y = 
reduce1 x y (y == 0)
where 
d  = gcd x y
reduce0 x y True = x `quot` d :% (y `quot` d)
reduce1 x y True = error []
reduce1 x y False = reduce0 x y otherwise



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
HASKELL
                  ↳ LetRed

mainModule Main
  (((<=) :: Ord a => a  ->  a  ->  Bool) :: Ord a => a  ->  a  ->  Bool)

module Main where
  import qualified Prelude



Let/Where Reductions:
The bindings of the following Let/Where expression
reduce1 x y (y == 0)
where 
d  = gcd x y
reduce0 x y True = x `quot` d :% (y `quot` d)
reduce1 x y True = error []
reduce1 x y False = reduce0 x y otherwise

are unpacked to the following functions on top level
reduce2D vwv vww = gcd vwv vww

reduce2Reduce0 vwv vww x y True = x `quot` reduce2D vwv vww :% (y `quot` reduce2D vwv vww)

reduce2Reduce1 vwv vww x y True = error []
reduce2Reduce1 vwv vww x y False = reduce2Reduce0 vwv vww x y otherwise

The bindings of the following Let/Where expression
gcd' (abs x) (abs y)
where 
gcd' x zx = gcd'2 x zx
gcd' x y = gcd'0 x y
gcd'0 x y = gcd' y (x `rem` y)
gcd'1 True x zx = x
gcd'1 zy zz vuu = gcd'0 zz vuu
gcd'2 x zx = gcd'1 (zx == 0) x zx
gcd'2 vuv vuw = gcd'0 vuv vuw

are unpacked to the following functions on top level
gcd0Gcd'2 x zx = gcd0Gcd'1 (zx == 0) x zx
gcd0Gcd'2 vuv vuw = gcd0Gcd'0 vuv vuw

gcd0Gcd'1 True x zx = x
gcd0Gcd'1 zy zz vuu = gcd0Gcd'0 zz vuu

gcd0Gcd'0 x y = gcd0Gcd' y (x `rem` y)

gcd0Gcd' x zx = gcd0Gcd'2 x zx
gcd0Gcd' x y = gcd0Gcd'0 x y



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
HASKELL
                      ↳ NumRed

mainModule Main
  (((<=) :: Ord a => a  ->  a  ->  Bool) :: Ord a => a  ->  a  ->  Bool)

module Main where
  import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
HASKELL
                          ↳ Narrow

mainModule Main
  ((<=) :: Ord a => a  ->  a  ->  Bool)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(vwx1400), Succ(vwx1500)) → new_primEqNat(vwx1400, vwx1500)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(vwx5900), Succ(vwx41000)) → new_primPlusNat(vwx5900, vwx41000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(vwx3100), Succ(vwx4100)) → new_primMulNat(vwx3100, Succ(vwx4100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs1(Left(vwx140), Left(vwx150), app(ty_Maybe, de), df) → new_esEs(vwx140, vwx150, de)
new_esEs3(@3(vwx140, vwx141, vwx142), @3(vwx150, vwx151, vwx152), baf, bag, app(ty_[], bba)) → new_esEs0(vwx142, vwx152, bba)
new_esEs(Just(vwx140), Just(vwx150), app(app(ty_Either, bc), bd)) → new_esEs1(vwx140, vwx150, bc, bd)
new_esEs3(@3(vwx140, vwx141, vwx142), @3(vwx150, vwx151, vwx152), baf, bag, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs3(vwx142, vwx152, bbf, bbg, bbh)
new_esEs1(Left(vwx140), Left(vwx150), app(ty_[], dg), df) → new_esEs0(vwx140, vwx150, dg)
new_esEs2(@2(vwx140, vwx141), @2(vwx150, vwx151), app(ty_[], hf), he) → new_esEs0(vwx140, vwx150, hf)
new_esEs3(@3(vwx140, vwx141, vwx142), @3(vwx150, vwx151, vwx152), baf, app(ty_[], bcc), bcb) → new_esEs0(vwx141, vwx151, bcc)
new_esEs2(@2(vwx140, vwx141), @2(vwx150, vwx151), gb, app(app(ty_@2, gg), gh)) → new_esEs2(vwx141, vwx151, gg, gh)
new_esEs2(@2(vwx140, vwx141), @2(vwx150, vwx151), gb, app(ty_Maybe, gc)) → new_esEs(vwx141, vwx151, gc)
new_esEs2(@2(vwx140, vwx141), @2(vwx150, vwx151), app(ty_Maybe, hd), he) → new_esEs(vwx140, vwx150, hd)
new_esEs3(@3(vwx140, vwx141, vwx142), @3(vwx150, vwx151, vwx152), app(ty_Maybe, bdc), bag, bcb) → new_esEs(vwx140, vwx150, bdc)
new_esEs(Just(vwx140), Just(vwx150), app(app(app(ty_@3, bg), bh), ca)) → new_esEs3(vwx140, vwx150, bg, bh, ca)
new_esEs3(@3(vwx140, vwx141, vwx142), @3(vwx150, vwx151, vwx152), app(ty_[], bdd), bag, bcb) → new_esEs0(vwx140, vwx150, bdd)
new_esEs2(@2(vwx140, vwx141), @2(vwx150, vwx151), app(app(ty_@2, baa), bab), he) → new_esEs2(vwx140, vwx150, baa, bab)
new_esEs2(@2(vwx140, vwx141), @2(vwx150, vwx151), gb, app(app(app(ty_@3, ha), hb), hc)) → new_esEs3(vwx141, vwx151, ha, hb, hc)
new_esEs1(Left(vwx140), Left(vwx150), app(app(ty_Either, dh), ea), df) → new_esEs1(vwx140, vwx150, dh, ea)
new_esEs1(Right(vwx140), Right(vwx150), eg, app(ty_[], fa)) → new_esEs0(vwx140, vwx150, fa)
new_esEs(Just(vwx140), Just(vwx150), app(ty_Maybe, ba)) → new_esEs(vwx140, vwx150, ba)
new_esEs0(:(vwx140, vwx141), :(vwx150, vwx151), app(ty_Maybe, cc)) → new_esEs(vwx140, vwx150, cc)
new_esEs1(Right(vwx140), Right(vwx150), eg, app(app(ty_Either, fb), fc)) → new_esEs1(vwx140, vwx150, fb, fc)
new_esEs3(@3(vwx140, vwx141, vwx142), @3(vwx150, vwx151, vwx152), app(app(ty_Either, bde), bdf), bag, bcb) → new_esEs1(vwx140, vwx150, bde, bdf)
new_esEs3(@3(vwx140, vwx141, vwx142), @3(vwx150, vwx151, vwx152), baf, app(ty_Maybe, bca), bcb) → new_esEs(vwx141, vwx151, bca)
new_esEs1(Left(vwx140), Left(vwx150), app(app(ty_@2, eb), ec), df) → new_esEs2(vwx140, vwx150, eb, ec)
new_esEs(Just(vwx140), Just(vwx150), app(ty_[], bb)) → new_esEs0(vwx140, vwx150, bb)
new_esEs3(@3(vwx140, vwx141, vwx142), @3(vwx150, vwx151, vwx152), baf, bag, app(ty_Maybe, bah)) → new_esEs(vwx142, vwx152, bah)
new_esEs2(@2(vwx140, vwx141), @2(vwx150, vwx151), gb, app(app(ty_Either, ge), gf)) → new_esEs1(vwx141, vwx151, ge, gf)
new_esEs3(@3(vwx140, vwx141, vwx142), @3(vwx150, vwx151, vwx152), baf, app(app(ty_Either, bcd), bce), bcb) → new_esEs1(vwx141, vwx151, bcd, bce)
new_esEs(Just(vwx140), Just(vwx150), app(app(ty_@2, be), bf)) → new_esEs2(vwx140, vwx150, be, bf)
new_esEs3(@3(vwx140, vwx141, vwx142), @3(vwx150, vwx151, vwx152), baf, app(app(app(ty_@3, bch), bda), bdb), bcb) → new_esEs3(vwx141, vwx151, bch, bda, bdb)
new_esEs3(@3(vwx140, vwx141, vwx142), @3(vwx150, vwx151, vwx152), baf, bag, app(app(ty_@2, bbd), bbe)) → new_esEs2(vwx142, vwx152, bbd, bbe)
new_esEs3(@3(vwx140, vwx141, vwx142), @3(vwx150, vwx151, vwx152), baf, app(app(ty_@2, bcf), bcg), bcb) → new_esEs2(vwx141, vwx151, bcf, bcg)
new_esEs3(@3(vwx140, vwx141, vwx142), @3(vwx150, vwx151, vwx152), app(app(ty_@2, bdg), bdh), bag, bcb) → new_esEs2(vwx140, vwx150, bdg, bdh)
new_esEs1(Right(vwx140), Right(vwx150), eg, app(app(app(ty_@3, fg), fh), ga)) → new_esEs3(vwx140, vwx150, fg, fh, ga)
new_esEs1(Right(vwx140), Right(vwx150), eg, app(app(ty_@2, fd), ff)) → new_esEs2(vwx140, vwx150, fd, ff)
new_esEs0(:(vwx140, vwx141), :(vwx150, vwx151), app(app(app(ty_@3, db), dc), dd)) → new_esEs3(vwx140, vwx150, db, dc, dd)
new_esEs0(:(vwx140, vwx141), :(vwx150, vwx151), app(app(ty_Either, ce), cf)) → new_esEs1(vwx140, vwx150, ce, cf)
new_esEs2(@2(vwx140, vwx141), @2(vwx150, vwx151), gb, app(ty_[], gd)) → new_esEs0(vwx141, vwx151, gd)
new_esEs3(@3(vwx140, vwx141, vwx142), @3(vwx150, vwx151, vwx152), baf, bag, app(app(ty_Either, bbb), bbc)) → new_esEs1(vwx142, vwx152, bbb, bbc)
new_esEs0(:(vwx140, vwx141), :(vwx150, vwx151), app(ty_[], cd)) → new_esEs0(vwx140, vwx150, cd)
new_esEs1(Right(vwx140), Right(vwx150), eg, app(ty_Maybe, eh)) → new_esEs(vwx140, vwx150, eh)
new_esEs1(Left(vwx140), Left(vwx150), app(app(app(ty_@3, ed), ee), ef), df) → new_esEs3(vwx140, vwx150, ed, ee, ef)
new_esEs0(:(vwx140, vwx141), :(vwx150, vwx151), app(app(ty_@2, cg), da)) → new_esEs2(vwx140, vwx150, cg, da)
new_esEs2(@2(vwx140, vwx141), @2(vwx150, vwx151), app(app(ty_Either, hg), hh), he) → new_esEs1(vwx140, vwx150, hg, hh)
new_esEs0(:(vwx140, vwx141), :(vwx150, vwx151), cb) → new_esEs0(vwx141, vwx151, cb)
new_esEs3(@3(vwx140, vwx141, vwx142), @3(vwx150, vwx151, vwx152), app(app(app(ty_@3, bea), beb), bec), bag, bcb) → new_esEs3(vwx140, vwx150, bea, beb, bec)
new_esEs2(@2(vwx140, vwx141), @2(vwx150, vwx151), app(app(app(ty_@3, bac), bad), bae), he) → new_esEs3(vwx140, vwx150, bac, bad, bae)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primCmpNat(Succ(vwx300), Succ(vwx400)) → new_primCmpNat(vwx300, vwx400)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_compare(:(vwx30, vwx31), :(vwx40, vwx41), baf) → new_primCompAux(vwx30, vwx40, new_compare4(vwx31, vwx41, baf), baf)
new_ltEs0(Just(vwx30), Just(vwx40), app(app(app(ty_@3, ea), eb), ec)) → new_ltEs1(vwx30, vwx40, ea, eb, ec)
new_lt(vwx30, vwx40, eg, eh) → new_compare2(vwx30, vwx40, new_esEs4(vwx30, vwx40, eg, eh), eg, eh)
new_primCompAux(vwx30, vwx40, vwx41, app(app(ty_@2, bbf), bbg)) → new_compare5(vwx30, vwx40, bbf, bbg)
new_ltEs1(@3(vwx30, vwx31, vwx32), @3(vwx40, vwx41, vwx42), gc, app(ty_[], hb), fb) → new_lt2(vwx31, vwx41, hb)
new_ltEs1(@3(vwx30, vwx31, vwx32), @3(vwx40, vwx41, vwx42), gc, app(app(app(ty_@3, gg), gh), ha), fb) → new_lt1(vwx31, vwx41, gg, gh, ha)
new_compare22(vwx30, vwx40, False, ga, gb) → new_ltEs3(vwx30, vwx40, ga, gb)
new_ltEs3(@2(vwx30, vwx31), @2(vwx40, vwx41), app(app(app(ty_@3, bcd), bce), bcf), bcb) → new_lt1(vwx30, vwx40, bcd, bce, bcf)
new_compare2(vwx30, vwx40, False, eg, eh) → new_ltEs(vwx30, vwx40, eg, eh)
new_ltEs1(@3(vwx30, vwx31, vwx32), @3(vwx40, vwx41, vwx42), gc, fa, app(app(ty_@2, bad), bae)) → new_ltEs3(vwx32, vwx42, bad, bae)
new_ltEs(Left(vwx30), Left(vwx40), app(app(ty_Either, ba), bb), bc) → new_ltEs(vwx30, vwx40, ba, bb)
new_ltEs(Right(vwx30), Right(vwx40), cc, app(app(ty_Either, cd), ce)) → new_ltEs(vwx30, vwx40, cd, ce)
new_ltEs0(Just(vwx30), Just(vwx40), app(app(ty_@2, ee), ef)) → new_ltEs3(vwx30, vwx40, ee, ef)
new_ltEs3(@2(vwx30, vwx31), @2(vwx40, vwx41), bdb, app(ty_Maybe, bde)) → new_ltEs0(vwx31, vwx41, bde)
new_ltEs3(@2(vwx30, vwx31), @2(vwx40, vwx41), bdb, app(app(app(ty_@3, bdf), bdg), bdh)) → new_ltEs1(vwx31, vwx41, bdf, bdg, bdh)
new_compare21(vwx30, vwx40, False, fd, ff, fg) → new_ltEs1(vwx30, vwx40, fd, ff, fg)
new_ltEs3(@2(vwx30, vwx31), @2(vwx40, vwx41), bdb, app(ty_[], bea)) → new_ltEs2(vwx31, vwx41, bea)
new_ltEs1(@3(vwx30, vwx31, vwx32), @3(vwx40, vwx41, vwx42), gc, app(ty_Maybe, gf), fb) → new_lt0(vwx31, vwx41, gf)
new_ltEs1(@3(vwx30, vwx31, vwx32), @3(vwx40, vwx41, vwx42), app(ty_[], fh), fa, fb) → new_compare(vwx30, vwx40, fh)
new_ltEs1(@3(vwx30, vwx31, vwx32), @3(vwx40, vwx41, vwx42), gc, app(app(ty_@2, hc), hd), fb) → new_lt3(vwx31, vwx41, hc, hd)
new_primCompAux(vwx30, vwx40, vwx41, app(app(ty_Either, bag), bah)) → new_compare0(vwx30, vwx40, bag, bah)
new_ltEs0(Just(vwx30), Just(vwx40), app(ty_Maybe, dh)) → new_ltEs0(vwx30, vwx40, dh)
new_ltEs1(@3(vwx30, vwx31, vwx32), @3(vwx40, vwx41, vwx42), app(app(ty_@2, ga), gb), fa, fb) → new_compare22(vwx30, vwx40, new_esEs7(vwx30, vwx40, ga, gb), ga, gb)
new_lt3(vwx30, vwx40, ga, gb) → new_compare22(vwx30, vwx40, new_esEs7(vwx30, vwx40, ga, gb), ga, gb)
new_primCompAux(vwx30, vwx40, vwx41, app(ty_[], bbe)) → new_compare(vwx30, vwx40, bbe)
new_ltEs(Left(vwx30), Left(vwx40), app(app(ty_@2, ca), cb), bc) → new_ltEs3(vwx30, vwx40, ca, cb)
new_ltEs(Right(vwx30), Right(vwx40), cc, app(app(app(ty_@3, cg), da), db)) → new_ltEs1(vwx30, vwx40, cg, da, db)
new_ltEs1(@3(vwx30, vwx31, vwx32), @3(vwx40, vwx41, vwx42), app(ty_Maybe, fc), fa, fb) → new_compare20(vwx30, vwx40, new_esEs5(vwx30, vwx40, fc), fc)
new_compare1(vwx30, vwx40, fc) → new_compare20(vwx30, vwx40, new_esEs5(vwx30, vwx40, fc), fc)
new_ltEs3(@2(vwx30, vwx31), @2(vwx40, vwx41), bdb, app(app(ty_@2, beb), bec)) → new_ltEs3(vwx31, vwx41, beb, bec)
new_ltEs1(@3(vwx30, vwx31, vwx32), @3(vwx40, vwx41, vwx42), app(app(app(ty_@3, fd), ff), fg), fa, fb) → new_compare21(vwx30, vwx40, new_esEs6(vwx30, vwx40, fd, ff, fg), fd, ff, fg)
new_ltEs3(@2(vwx30, vwx31), @2(vwx40, vwx41), app(ty_Maybe, bcc), bcb) → new_lt0(vwx30, vwx40, bcc)
new_ltEs(Right(vwx30), Right(vwx40), cc, app(app(ty_@2, dd), de)) → new_ltEs3(vwx30, vwx40, dd, de)
new_compare3(vwx30, vwx40, fd, ff, fg) → new_compare21(vwx30, vwx40, new_esEs6(vwx30, vwx40, fd, ff, fg), fd, ff, fg)
new_ltEs3(@2(vwx30, vwx31), @2(vwx40, vwx41), bdb, app(app(ty_Either, bdc), bdd)) → new_ltEs(vwx31, vwx41, bdc, bdd)
new_ltEs3(@2(vwx30, vwx31), @2(vwx40, vwx41), app(app(ty_@2, bch), bda), bcb) → new_lt3(vwx30, vwx40, bch, bda)
new_ltEs2(:(vwx30, vwx31), :(vwx40, vwx41), baf) → new_compare(vwx31, vwx41, baf)
new_ltEs1(@3(vwx30, vwx31, vwx32), @3(vwx40, vwx41, vwx42), gc, fa, app(ty_[], bac)) → new_ltEs2(vwx32, vwx42, bac)
new_ltEs2(:(vwx30, vwx31), :(vwx40, vwx41), baf) → new_primCompAux(vwx30, vwx40, new_compare4(vwx31, vwx41, baf), baf)
new_ltEs0(Just(vwx30), Just(vwx40), app(ty_[], ed)) → new_ltEs2(vwx30, vwx40, ed)
new_compare(:(vwx30, vwx31), :(vwx40, vwx41), baf) → new_compare(vwx31, vwx41, baf)
new_primCompAux(vwx30, vwx40, vwx41, app(ty_Maybe, bba)) → new_compare1(vwx30, vwx40, bba)
new_primCompAux(vwx30, vwx40, vwx41, app(app(app(ty_@3, bbb), bbc), bbd)) → new_compare3(vwx30, vwx40, bbb, bbc, bbd)
new_ltEs(Left(vwx30), Left(vwx40), app(ty_Maybe, bd), bc) → new_ltEs0(vwx30, vwx40, bd)
new_compare5(vwx30, vwx40, ga, gb) → new_compare22(vwx30, vwx40, new_esEs7(vwx30, vwx40, ga, gb), ga, gb)
new_ltEs1(@3(vwx30, vwx31, vwx32), @3(vwx40, vwx41, vwx42), gc, fa, app(app(app(ty_@3, hh), baa), bab)) → new_ltEs1(vwx32, vwx42, hh, baa, bab)
new_ltEs(Left(vwx30), Left(vwx40), app(app(app(ty_@3, be), bf), bg), bc) → new_ltEs1(vwx30, vwx40, be, bf, bg)
new_lt2(vwx30, vwx40, fh) → new_compare(vwx30, vwx40, fh)
new_ltEs1(@3(vwx30, vwx31, vwx32), @3(vwx40, vwx41, vwx42), gc, fa, app(ty_Maybe, hg)) → new_ltEs0(vwx32, vwx42, hg)
new_ltEs3(@2(vwx30, vwx31), @2(vwx40, vwx41), app(app(ty_Either, bbh), bca), bcb) → new_lt(vwx30, vwx40, bbh, bca)
new_lt1(vwx30, vwx40, fd, ff, fg) → new_compare21(vwx30, vwx40, new_esEs6(vwx30, vwx40, fd, ff, fg), fd, ff, fg)
new_compare0(vwx30, vwx40, eg, eh) → new_compare2(vwx30, vwx40, new_esEs4(vwx30, vwx40, eg, eh), eg, eh)
new_ltEs(Left(vwx30), Left(vwx40), app(ty_[], bh), bc) → new_ltEs2(vwx30, vwx40, bh)
new_ltEs(Right(vwx30), Right(vwx40), cc, app(ty_[], dc)) → new_ltEs2(vwx30, vwx40, dc)
new_ltEs(Right(vwx30), Right(vwx40), cc, app(ty_Maybe, cf)) → new_ltEs0(vwx30, vwx40, cf)
new_compare20(vwx30, vwx40, False, fc) → new_ltEs0(vwx30, vwx40, fc)
new_ltEs1(@3(vwx30, vwx31, vwx32), @3(vwx40, vwx41, vwx42), gc, fa, app(app(ty_Either, he), hf)) → new_ltEs(vwx32, vwx42, he, hf)
new_ltEs1(@3(vwx30, vwx31, vwx32), @3(vwx40, vwx41, vwx42), app(app(ty_Either, eg), eh), fa, fb) → new_compare2(vwx30, vwx40, new_esEs4(vwx30, vwx40, eg, eh), eg, eh)
new_ltEs1(@3(vwx30, vwx31, vwx32), @3(vwx40, vwx41, vwx42), gc, app(app(ty_Either, gd), ge), fb) → new_lt(vwx31, vwx41, gd, ge)
new_lt0(vwx30, vwx40, fc) → new_compare20(vwx30, vwx40, new_esEs5(vwx30, vwx40, fc), fc)
new_ltEs0(Just(vwx30), Just(vwx40), app(app(ty_Either, df), dg)) → new_ltEs(vwx30, vwx40, df, dg)
new_ltEs3(@2(vwx30, vwx31), @2(vwx40, vwx41), app(ty_[], bcg), bcb) → new_lt2(vwx30, vwx40, bcg)

The TRS R consists of the following rules:

new_esEs22(vwx140, vwx150, ty_Double) → new_esEs17(vwx140, vwx150)
new_compare8(vwx30, vwx40, app(app(ty_Either, bag), bah)) → new_compare6(vwx30, vwx40, bag, bah)
new_lt20(vwx31, vwx41, ty_Int) → new_lt16(vwx31, vwx41)
new_lt19(vwx30, vwx40, app(ty_Ratio, cdb)) → new_lt10(vwx30, vwx40, cdb)
new_lt11(vwx30, vwx40, ty_Bool) → new_lt17(vwx30, vwx40)
new_compare9(Char(vwx30), Char(vwx40)) → new_primCmpNat0(vwx30, vwx40)
new_ltEs15(EQ, LT) → False
new_ltEs19(vwx32, vwx42, app(ty_Ratio, ceh)) → new_ltEs16(vwx32, vwx42, ceh)
new_esEs23(vwx141, vwx151, ty_Integer) → new_esEs19(vwx141, vwx151)
new_ltEs19(vwx32, vwx42, app(ty_[], bac)) → new_ltEs9(vwx32, vwx42, bac)
new_esEs20(vwx142, vwx152, ty_Bool) → new_esEs12(vwx142, vwx152)
new_lt11(vwx30, vwx40, ty_Ordering) → new_lt5(vwx30, vwx40)
new_esEs20(vwx142, vwx152, ty_@0) → new_esEs8(vwx142, vwx152)
new_esEs27(vwx140, vwx150, app(ty_Ratio, cgg)) → new_esEs18(vwx140, vwx150, cgg)
new_compare10(vwx30, vwx40, True, eg, eh) → LT
new_esEs4(Right(vwx140), Right(vwx150), bfb, app(app(app(ty_@3, dbg), dbh), dca)) → new_esEs6(vwx140, vwx150, dbg, dbh, dca)
new_esEs26(vwx141, vwx151, ty_Float) → new_esEs10(vwx141, vwx151)
new_esEs14(vwx14, vwx15, app(app(app(ty_@3, bfg), bfh), bga)) → new_esEs6(vwx14, vwx15, bfg, bfh, bga)
new_esEs5(Just(vwx140), Just(vwx150), app(ty_[], cca)) → new_esEs15(vwx140, vwx150, cca)
new_ltEs6(Nothing, Just(vwx40), bee) → True
new_lt19(vwx30, vwx40, ty_@0) → new_lt8(vwx30, vwx40)
new_ltEs10(vwx3, vwx4) → new_not(new_compare13(vwx3, vwx4))
new_ltEs15(EQ, EQ) → True
new_esEs4(Right(vwx140), Right(vwx150), bfb, app(ty_Maybe, dah)) → new_esEs5(vwx140, vwx150, dah)
new_primMulNat0(Zero, Zero) → Zero
new_esEs12(True, True) → True
new_ltEs11(vwx3, vwx4) → new_not(new_compare14(vwx3, vwx4))
new_esEs4(Right(vwx140), Right(vwx150), bfb, app(ty_Ratio, dbd)) → new_esEs18(vwx140, vwx150, dbd)
new_lt20(vwx31, vwx41, ty_@0) → new_lt8(vwx31, vwx41)
new_esEs4(Left(vwx140), Left(vwx150), app(ty_[], chg), bfc) → new_esEs15(vwx140, vwx150, chg)
new_esEs27(vwx140, vwx150, app(ty_[], cgd)) → new_esEs15(vwx140, vwx150, cgd)
new_esEs4(Left(vwx140), Left(vwx150), ty_Char, bfc) → new_esEs16(vwx140, vwx150)
new_ltEs18(vwx31, vwx41, app(app(app(ty_@3, bdf), bdg), bdh)) → new_ltEs8(vwx31, vwx41, bdf, bdg, bdh)
new_esEs9(LT) → True
new_esEs21(vwx141, vwx151, app(ty_[], bhe)) → new_esEs15(vwx141, vwx151, bhe)
new_esEs4(Left(vwx140), Left(vwx150), ty_Int, bfc) → new_esEs11(vwx140, vwx150)
new_compare6(vwx30, vwx40, eg, eh) → new_compare23(vwx30, vwx40, new_esEs4(vwx30, vwx40, eg, eh), eg, eh)
new_esEs4(Right(vwx140), Right(vwx150), bfb, app(ty_[], dba)) → new_esEs15(vwx140, vwx150, dba)
new_ltEs14(False, True) → True
new_esEs25(vwx140, vwx150, app(ty_Ratio, cdg)) → new_esEs18(vwx140, vwx150, cdg)
new_esEs13(EQ, EQ) → True
new_esEs14(vwx14, vwx15, ty_Ordering) → new_esEs13(vwx14, vwx15)
new_compare8(vwx30, vwx40, ty_Integer) → new_compare14(vwx30, vwx40)
new_not(GT) → False
new_lt19(vwx30, vwx40, app(app(app(ty_@3, fd), ff), fg)) → new_lt9(vwx30, vwx40, fd, ff, fg)
new_ltEs18(vwx31, vwx41, app(ty_[], bea)) → new_ltEs9(vwx31, vwx41, bea)
new_lt7(vwx30, vwx40, fc) → new_esEs9(new_compare11(vwx30, vwx40, fc))
new_compare29(vwx30, vwx40, False, ga, gb) → new_compare114(vwx30, vwx40, new_ltEs12(vwx30, vwx40, ga, gb), ga, gb)
new_ltEs15(GT, LT) → False
new_ltEs6(Just(vwx30), Just(vwx40), app(app(app(ty_@3, ea), eb), ec)) → new_ltEs8(vwx30, vwx40, ea, eb, ec)
new_esEs20(vwx142, vwx152, app(app(ty_Either, bgd), bge)) → new_esEs4(vwx142, vwx152, bgd, bge)
new_ltEs6(Just(vwx30), Just(vwx40), ty_Int) → new_ltEs13(vwx30, vwx40)
new_esEs21(vwx141, vwx151, ty_Integer) → new_esEs19(vwx141, vwx151)
new_lt19(vwx30, vwx40, ty_Bool) → new_lt17(vwx30, vwx40)
new_esEs5(Just(vwx140), Just(vwx150), app(ty_Maybe, cbh)) → new_esEs5(vwx140, vwx150, cbh)
new_compare19(:%(vwx30, vwx31), :%(vwx40, vwx41), ty_Integer) → new_compare14(new_sr0(vwx30, vwx41), new_sr0(vwx40, vwx31))
new_esEs22(vwx140, vwx150, app(ty_Ratio, cbb)) → new_esEs18(vwx140, vwx150, cbb)
new_compare15(vwx30, vwx40, ga, gb) → new_compare29(vwx30, vwx40, new_esEs7(vwx30, vwx40, ga, gb), ga, gb)
new_compare8(vwx30, vwx40, ty_@0) → new_compare13(vwx30, vwx40)
new_ltEs19(vwx32, vwx42, app(app(ty_Either, he), hf)) → new_ltEs4(vwx32, vwx42, he, hf)
new_ltEs19(vwx32, vwx42, ty_Ordering) → new_ltEs15(vwx32, vwx42)
new_esEs13(EQ, LT) → False
new_esEs13(LT, EQ) → False
new_esEs25(vwx140, vwx150, app(app(ty_@2, cdh), cea)) → new_esEs7(vwx140, vwx150, cdh, cea)
new_esEs25(vwx140, vwx150, app(app(ty_Either, cde), cdf)) → new_esEs4(vwx140, vwx150, cde, cdf)
new_esEs22(vwx140, vwx150, ty_Ordering) → new_esEs13(vwx140, vwx150)
new_esEs22(vwx140, vwx150, app(app(ty_Either, cah), cba)) → new_esEs4(vwx140, vwx150, cah, cba)
new_ltEs15(EQ, GT) → True
new_esEs21(vwx141, vwx151, ty_Ordering) → new_esEs13(vwx141, vwx151)
new_lt19(vwx30, vwx40, app(ty_Maybe, fc)) → new_lt7(vwx30, vwx40, fc)
new_lt11(vwx30, vwx40, app(app(ty_Either, bbh), bca)) → new_lt4(vwx30, vwx40, bbh, bca)
new_lt11(vwx30, vwx40, ty_Float) → new_lt18(vwx30, vwx40)
new_compare8(vwx30, vwx40, app(app(app(ty_@3, bbb), bbc), bbd)) → new_compare12(vwx30, vwx40, bbb, bbc, bbd)
new_esEs24(vwx140, vwx150, ty_Integer) → new_esEs19(vwx140, vwx150)
new_esEs26(vwx141, vwx151, ty_Int) → new_esEs11(vwx141, vwx151)
new_lt20(vwx31, vwx41, ty_Double) → new_lt12(vwx31, vwx41)
new_lt11(vwx30, vwx40, app(app(app(ty_@3, bcd), bce), bcf)) → new_lt9(vwx30, vwx40, bcd, bce, bcf)
new_esEs26(vwx141, vwx151, ty_Bool) → new_esEs12(vwx141, vwx151)
new_esEs22(vwx140, vwx150, ty_Int) → new_esEs11(vwx140, vwx150)
new_lt12(vwx30, vwx40) → new_esEs9(new_compare7(vwx30, vwx40))
new_esEs14(vwx14, vwx15, app(app(ty_@2, bfe), bff)) → new_esEs7(vwx14, vwx15, bfe, bff)
new_ltEs4(Right(vwx30), Right(vwx40), cc, app(app(ty_Either, cd), ce)) → new_ltEs4(vwx30, vwx40, cd, ce)
new_ltEs4(Right(vwx30), Right(vwx40), cc, ty_Bool) → new_ltEs14(vwx30, vwx40)
new_esEs21(vwx141, vwx151, ty_@0) → new_esEs8(vwx141, vwx151)
new_ltEs4(Left(vwx30), Right(vwx40), cc, bc) → True
new_ltEs18(vwx31, vwx41, ty_Int) → new_ltEs13(vwx31, vwx41)
new_ltEs15(LT, LT) → True
new_primCmpNat0(Zero, Succ(vwx400)) → LT
new_ltEs4(Left(vwx30), Left(vwx40), ty_Bool, bc) → new_ltEs14(vwx30, vwx40)
new_compare8(vwx30, vwx40, ty_Int) → new_compare16(vwx30, vwx40)
new_esEs26(vwx141, vwx151, ty_Double) → new_esEs17(vwx141, vwx151)
new_lt10(vwx30, vwx40, cdb) → new_esEs9(new_compare19(vwx30, vwx40, cdb))
new_esEs4(Right(vwx140), Right(vwx150), bfb, app(app(ty_@2, dbe), dbf)) → new_esEs7(vwx140, vwx150, dbe, dbf)
new_primCompAux0(vwx30, vwx40, vwx41, baf) → new_primCompAux00(vwx41, new_compare8(vwx30, vwx40, baf))
new_compare25(vwx30, vwx40, False, fd, ff, fg) → new_compare111(vwx30, vwx40, new_ltEs8(vwx30, vwx40, fd, ff, fg), fd, ff, fg)
new_compare25(vwx30, vwx40, True, fd, ff, fg) → EQ
new_esEs7(@2(vwx140, vwx141), @2(vwx150, vwx151), bfe, bff) → new_asAs(new_esEs27(vwx140, vwx150, bfe), new_esEs26(vwx141, vwx151, bff))
new_esEs25(vwx140, vwx150, ty_Double) → new_esEs17(vwx140, vwx150)
new_esEs27(vwx140, vwx150, ty_Ordering) → new_esEs13(vwx140, vwx150)
new_esEs20(vwx142, vwx152, app(app(app(ty_@3, bha), bhb), bhc)) → new_esEs6(vwx142, vwx152, bha, bhb, bhc)
new_ltEs4(Right(vwx30), Right(vwx40), cc, ty_@0) → new_ltEs10(vwx30, vwx40)
new_ltEs19(vwx32, vwx42, ty_Int) → new_ltEs13(vwx32, vwx42)
new_primEqNat0(Zero, Zero) → True
new_esEs20(vwx142, vwx152, ty_Int) → new_esEs11(vwx142, vwx152)
new_compare26(vwx30, vwx40, True) → EQ
new_esEs14(vwx14, vwx15, ty_Char) → new_esEs16(vwx14, vwx15)
new_lt11(vwx30, vwx40, app(ty_Ratio, cee)) → new_lt10(vwx30, vwx40, cee)
new_compare12(vwx30, vwx40, fd, ff, fg) → new_compare25(vwx30, vwx40, new_esEs6(vwx30, vwx40, fd, ff, fg), fd, ff, fg)
new_compare29(vwx30, vwx40, True, ga, gb) → EQ
new_esEs13(GT, LT) → False
new_esEs13(LT, GT) → False
new_lt11(vwx30, vwx40, ty_Integer) → new_lt15(vwx30, vwx40)
new_lt19(vwx30, vwx40, ty_Ordering) → new_lt5(vwx30, vwx40)
new_esEs4(Left(vwx140), Left(vwx150), ty_Ordering, bfc) → new_esEs13(vwx140, vwx150)
new_esEs22(vwx140, vwx150, app(app(ty_@2, cbc), cbd)) → new_esEs7(vwx140, vwx150, cbc, cbd)
new_esEs4(Left(vwx140), Left(vwx150), ty_Integer, bfc) → new_esEs19(vwx140, vwx150)
new_lt11(vwx30, vwx40, ty_@0) → new_lt8(vwx30, vwx40)
new_ltEs4(Left(vwx30), Left(vwx40), ty_Float, bc) → new_ltEs17(vwx30, vwx40)
new_sr(vwx31, vwx41) → new_primMulInt(vwx31, vwx41)
new_ltEs9(vwx3, vwx4, baf) → new_not(new_compare4(vwx3, vwx4, baf))
new_esEs25(vwx140, vwx150, app(ty_[], cdd)) → new_esEs15(vwx140, vwx150, cdd)
new_compare8(vwx30, vwx40, ty_Float) → new_compare24(vwx30, vwx40)
new_ltEs15(GT, GT) → True
new_ltEs4(Right(vwx30), Right(vwx40), cc, ty_Ordering) → new_ltEs15(vwx30, vwx40)
new_ltEs4(Left(vwx30), Left(vwx40), ty_Int, bc) → new_ltEs13(vwx30, vwx40)
new_esEs4(Right(vwx140), Right(vwx150), bfb, ty_Ordering) → new_esEs13(vwx140, vwx150)
new_compare4([], [], baf) → EQ
new_primPlusNat0(Succ(vwx590), vwx4100) → Succ(Succ(new_primPlusNat1(vwx590, vwx4100)))
new_esEs4(Right(vwx140), Right(vwx150), bfb, ty_@0) → new_esEs8(vwx140, vwx150)
new_ltEs6(Just(vwx30), Just(vwx40), ty_Integer) → new_ltEs11(vwx30, vwx40)
new_esEs5(Just(vwx140), Just(vwx150), ty_Double) → new_esEs17(vwx140, vwx150)
new_lt8(vwx30, vwx40) → new_esEs9(new_compare13(vwx30, vwx40))
new_esEs26(vwx141, vwx151, app(app(app(ty_@3, cfh), cga), cgb)) → new_esEs6(vwx141, vwx151, cfh, cga, cgb)
new_esEs12(False, False) → True
new_esEs22(vwx140, vwx150, ty_Char) → new_esEs16(vwx140, vwx150)
new_esEs16(Char(vwx140), Char(vwx150)) → new_primEqNat0(vwx140, vwx150)
new_ltEs13(vwx3, vwx4) → new_not(new_compare16(vwx3, vwx4))
new_ltEs4(Left(vwx30), Left(vwx40), ty_@0, bc) → new_ltEs10(vwx30, vwx40)
new_esEs17(Double(vwx140, vwx141), Double(vwx150, vwx151)) → new_esEs11(new_sr(vwx140, vwx150), new_sr(vwx141, vwx151))
new_esEs4(Right(vwx140), Right(vwx150), bfb, app(app(ty_Either, dbb), dbc)) → new_esEs4(vwx140, vwx150, dbb, dbc)
new_lt18(vwx30, vwx40) → new_esEs9(new_compare24(vwx30, vwx40))
new_primEqInt(Neg(Succ(vwx1400)), Neg(Succ(vwx1500))) → new_primEqNat0(vwx1400, vwx1500)
new_compare18(vwx30, vwx40) → new_compare28(vwx30, vwx40, new_esEs13(vwx30, vwx40))
new_lt19(vwx30, vwx40, ty_Char) → new_lt13(vwx30, vwx40)
new_esEs9(GT) → False
new_esEs14(vwx14, vwx15, app(ty_Ratio, bfd)) → new_esEs18(vwx14, vwx15, bfd)
new_esEs22(vwx140, vwx150, app(app(app(ty_@3, cbe), cbf), cbg)) → new_esEs6(vwx140, vwx150, cbe, cbf, cbg)
new_ltEs19(vwx32, vwx42, ty_Double) → new_ltEs5(vwx32, vwx42)
new_esEs4(Left(vwx140), Left(vwx150), app(app(ty_Either, chh), daa), bfc) → new_esEs4(vwx140, vwx150, chh, daa)
new_primPlusNat1(Zero, Succ(vwx41000)) → Succ(vwx41000)
new_primPlusNat1(Succ(vwx5900), Zero) → Succ(vwx5900)
new_compare11(vwx30, vwx40, fc) → new_compare27(vwx30, vwx40, new_esEs5(vwx30, vwx40, fc), fc)
new_esEs6(@3(vwx140, vwx141, vwx142), @3(vwx150, vwx151, vwx152), bfg, bfh, bga) → new_asAs(new_esEs22(vwx140, vwx150, bfg), new_asAs(new_esEs21(vwx141, vwx151, bfh), new_esEs20(vwx142, vwx152, bga)))
new_esEs9(EQ) → False
new_ltEs6(Just(vwx30), Just(vwx40), ty_Double) → new_ltEs5(vwx30, vwx40)
new_lt20(vwx31, vwx41, app(app(ty_Either, gd), ge)) → new_lt4(vwx31, vwx41, gd, ge)
new_esEs5(Just(vwx140), Just(vwx150), ty_Int) → new_esEs11(vwx140, vwx150)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_ltEs5(vwx3, vwx4) → new_not(new_compare7(vwx3, vwx4))
new_esEs4(Left(vwx140), Left(vwx150), ty_Bool, bfc) → new_esEs12(vwx140, vwx150)
new_esEs26(vwx141, vwx151, ty_Integer) → new_esEs19(vwx141, vwx151)
new_esEs21(vwx141, vwx151, app(app(ty_@2, caa), cab)) → new_esEs7(vwx141, vwx151, caa, cab)
new_lt19(vwx30, vwx40, ty_Integer) → new_lt15(vwx30, vwx40)
new_ltEs6(Just(vwx30), Just(vwx40), ty_Char) → new_ltEs7(vwx30, vwx40)
new_primEqInt(Neg(Succ(vwx1400)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(vwx1500))) → False
new_ltEs4(Left(vwx30), Left(vwx40), app(app(ty_Either, ba), bb), bc) → new_ltEs4(vwx30, vwx40, ba, bb)
new_lt14(vwx30, vwx40, fh) → new_esEs9(new_compare4(vwx30, vwx40, fh))
new_esEs22(vwx140, vwx150, ty_Integer) → new_esEs19(vwx140, vwx150)
new_ltEs6(Just(vwx30), Just(vwx40), ty_Bool) → new_ltEs14(vwx30, vwx40)
new_esEs21(vwx141, vwx151, app(app(ty_Either, bhf), bhg)) → new_esEs4(vwx141, vwx151, bhf, bhg)
new_ltEs6(Just(vwx30), Just(vwx40), app(app(ty_Either, df), dg)) → new_ltEs4(vwx30, vwx40, df, dg)
new_lt16(vwx30, vwx40) → new_esEs9(new_compare16(vwx30, vwx40))
new_esEs25(vwx140, vwx150, ty_Char) → new_esEs16(vwx140, vwx150)
new_compare19(:%(vwx30, vwx31), :%(vwx40, vwx41), ty_Int) → new_compare16(new_sr(vwx30, vwx41), new_sr(vwx40, vwx31))
new_primCmpInt(Neg(Zero), Pos(Zero)) → EQ
new_primCmpInt(Pos(Zero), Neg(Zero)) → EQ
new_ltEs15(LT, GT) → True
new_esEs21(vwx141, vwx151, ty_Float) → new_esEs10(vwx141, vwx151)
new_ltEs18(vwx31, vwx41, app(ty_Ratio, cef)) → new_ltEs16(vwx31, vwx41, cef)
new_primCmpNat0(Succ(vwx300), Succ(vwx400)) → new_primCmpNat0(vwx300, vwx400)
new_compare112(vwx30, vwx40, True) → LT
new_esEs13(LT, LT) → True
new_esEs5(Just(vwx140), Just(vwx150), ty_Char) → new_esEs16(vwx140, vwx150)
new_esEs4(Right(vwx140), Right(vwx150), bfb, ty_Integer) → new_esEs19(vwx140, vwx150)
new_primEqInt(Pos(Succ(vwx1400)), Pos(Succ(vwx1500))) → new_primEqNat0(vwx1400, vwx1500)
new_esEs4(Right(vwx140), Right(vwx150), bfb, ty_Int) → new_esEs11(vwx140, vwx150)
new_compare10(vwx30, vwx40, False, eg, eh) → GT
new_esEs25(vwx140, vwx150, app(ty_Maybe, cdc)) → new_esEs5(vwx140, vwx150, cdc)
new_ltEs4(Left(vwx30), Left(vwx40), app(app(app(ty_@3, be), bf), bg), bc) → new_ltEs8(vwx30, vwx40, be, bf, bg)
new_ltEs19(vwx32, vwx42, ty_Bool) → new_ltEs14(vwx32, vwx42)
new_ltEs18(vwx31, vwx41, ty_@0) → new_ltEs10(vwx31, vwx41)
new_compare8(vwx30, vwx40, app(ty_[], bbe)) → new_compare4(vwx30, vwx40, bbe)
new_lt11(vwx30, vwx40, app(ty_Maybe, bcc)) → new_lt7(vwx30, vwx40, bcc)
new_primEqNat0(Succ(vwx1400), Succ(vwx1500)) → new_primEqNat0(vwx1400, vwx1500)
new_ltEs14(False, False) → True
new_compare14(Integer(vwx30), Integer(vwx40)) → new_primCmpInt(vwx30, vwx40)
new_esEs27(vwx140, vwx150, ty_Char) → new_esEs16(vwx140, vwx150)
new_esEs22(vwx140, vwx150, ty_Bool) → new_esEs12(vwx140, vwx150)
new_lt19(vwx30, vwx40, app(app(ty_@2, ga), gb)) → new_lt6(vwx30, vwx40, ga, gb)
new_compare111(vwx30, vwx40, True, fd, ff, fg) → LT
new_esEs14(vwx14, vwx15, app(ty_Maybe, beh)) → new_esEs5(vwx14, vwx15, beh)
new_esEs20(vwx142, vwx152, ty_Float) → new_esEs10(vwx142, vwx152)
new_primCompAux00(vwx45, LT) → LT
new_lt17(vwx30, vwx40) → new_esEs9(new_compare17(vwx30, vwx40))
new_lt5(vwx30, vwx40) → new_esEs9(new_compare18(vwx30, vwx40))
new_esEs26(vwx141, vwx151, ty_@0) → new_esEs8(vwx141, vwx151)
new_compare114(vwx30, vwx40, True, ga, gb) → LT
new_primCmpInt(Neg(Succ(vwx300)), Neg(vwx40)) → new_primCmpNat0(vwx40, Succ(vwx300))
new_ltEs4(Left(vwx30), Left(vwx40), app(ty_Ratio, dcb), bc) → new_ltEs16(vwx30, vwx40, dcb)
new_lt11(vwx30, vwx40, app(app(ty_@2, bch), bda)) → new_lt6(vwx30, vwx40, bch, bda)
new_esEs10(Float(vwx140, vwx141), Float(vwx150, vwx151)) → new_esEs11(new_sr(vwx140, vwx150), new_sr(vwx141, vwx151))
new_esEs21(vwx141, vwx151, ty_Int) → new_esEs11(vwx141, vwx151)
new_ltEs4(Right(vwx30), Right(vwx40), cc, app(app(app(ty_@3, cg), da), db)) → new_ltEs8(vwx30, vwx40, cg, da, db)
new_ltEs18(vwx31, vwx41, app(app(ty_@2, beb), bec)) → new_ltEs12(vwx31, vwx41, beb, bec)
new_esEs15([], [], bfa) → True
new_primEqInt(Pos(Zero), Pos(Succ(vwx1500))) → False
new_primEqInt(Pos(Succ(vwx1400)), Pos(Zero)) → False
new_ltEs4(Left(vwx30), Left(vwx40), ty_Ordering, bc) → new_ltEs15(vwx30, vwx40)
new_ltEs19(vwx32, vwx42, app(ty_Maybe, hg)) → new_ltEs6(vwx32, vwx42, hg)
new_ltEs18(vwx31, vwx41, ty_Integer) → new_ltEs11(vwx31, vwx41)
new_lt15(vwx30, vwx40) → new_esEs9(new_compare14(vwx30, vwx40))
new_ltEs6(Just(vwx30), Nothing, bee) → False
new_ltEs8(@3(vwx30, vwx31, vwx32), @3(vwx40, vwx41, vwx42), gc, fa, fb) → new_pePe(new_lt19(vwx30, vwx40, gc), vwx30, vwx40, new_pePe(new_lt20(vwx31, vwx41, fa), vwx31, vwx41, new_ltEs19(vwx32, vwx42, fb), fa), gc)
new_ltEs19(vwx32, vwx42, ty_Float) → new_ltEs17(vwx32, vwx42)
new_primCmpNat0(Zero, Zero) → EQ
new_esEs4(Left(vwx140), Left(vwx150), ty_Double, bfc) → new_esEs17(vwx140, vwx150)
new_primCmpNat0(Succ(vwx300), Zero) → GT
new_lt11(vwx30, vwx40, ty_Char) → new_lt13(vwx30, vwx40)
new_primCmpInt(Neg(Zero), Pos(Succ(vwx400))) → LT
new_esEs21(vwx141, vwx151, ty_Char) → new_esEs16(vwx141, vwx151)
new_lt20(vwx31, vwx41, ty_Char) → new_lt13(vwx31, vwx41)
new_sr0(Integer(vwx400), Integer(vwx310)) → Integer(new_primMulInt(vwx400, vwx310))
new_primPlusNat1(Succ(vwx5900), Succ(vwx41000)) → Succ(Succ(new_primPlusNat1(vwx5900, vwx41000)))
new_ltEs19(vwx32, vwx42, app(app(ty_@2, bad), bae)) → new_ltEs12(vwx32, vwx42, bad, bae)
new_esEs21(vwx141, vwx151, ty_Double) → new_esEs17(vwx141, vwx151)
new_primEqInt(Neg(Succ(vwx1400)), Pos(vwx150)) → False
new_primEqInt(Pos(Succ(vwx1400)), Neg(vwx150)) → False
new_ltEs18(vwx31, vwx41, app(app(ty_Either, bdc), bdd)) → new_ltEs4(vwx31, vwx41, bdc, bdd)
new_esEs5(Just(vwx140), Just(vwx150), ty_Bool) → new_esEs12(vwx140, vwx150)
new_esEs27(vwx140, vwx150, app(ty_Maybe, cgc)) → new_esEs5(vwx140, vwx150, cgc)
new_compare8(vwx30, vwx40, ty_Char) → new_compare9(vwx30, vwx40)
new_esEs25(vwx140, vwx150, ty_@0) → new_esEs8(vwx140, vwx150)
new_ltEs6(Just(vwx30), Just(vwx40), app(ty_Maybe, dh)) → new_ltEs6(vwx30, vwx40, dh)
new_ltEs4(Left(vwx30), Left(vwx40), app(ty_[], bh), bc) → new_ltEs9(vwx30, vwx40, bh)
new_ltEs4(Right(vwx30), Right(vwx40), cc, app(ty_Maybe, cf)) → new_ltEs6(vwx30, vwx40, cf)
new_primEqInt(Pos(Zero), Neg(Succ(vwx1500))) → False
new_primEqInt(Neg(Zero), Pos(Succ(vwx1500))) → False
new_compare28(vwx30, vwx40, False) → new_compare112(vwx30, vwx40, new_ltEs15(vwx30, vwx40))
new_primCompAux00(vwx45, EQ) → vwx45
new_primCmpInt(Pos(Zero), Pos(Succ(vwx400))) → new_primCmpNat0(Zero, Succ(vwx400))
new_esEs27(vwx140, vwx150, app(app(ty_@2, cgh), cha)) → new_esEs7(vwx140, vwx150, cgh, cha)
new_esEs22(vwx140, vwx150, ty_@0) → new_esEs8(vwx140, vwx150)
new_lt20(vwx31, vwx41, app(app(app(ty_@3, gg), gh), ha)) → new_lt9(vwx31, vwx41, gg, gh, ha)
new_compare17(vwx30, vwx40) → new_compare26(vwx30, vwx40, new_esEs12(vwx30, vwx40))
new_esEs27(vwx140, vwx150, ty_Float) → new_esEs10(vwx140, vwx150)
new_ltEs4(Left(vwx30), Left(vwx40), app(ty_Maybe, bd), bc) → new_ltEs6(vwx30, vwx40, bd)
new_esEs4(Right(vwx140), Right(vwx150), bfb, ty_Float) → new_esEs10(vwx140, vwx150)
new_ltEs18(vwx31, vwx41, ty_Float) → new_ltEs17(vwx31, vwx41)
new_compare113(vwx30, vwx40, True) → LT
new_esEs11(vwx14, vwx15) → new_primEqInt(vwx14, vwx15)
new_compare114(vwx30, vwx40, False, ga, gb) → GT
new_ltEs4(Right(vwx30), Left(vwx40), cc, bc) → False
new_ltEs4(Left(vwx30), Left(vwx40), app(app(ty_@2, ca), cb), bc) → new_ltEs12(vwx30, vwx40, ca, cb)
new_primCmpInt(Pos(Succ(vwx300)), Pos(vwx40)) → new_primCmpNat0(Succ(vwx300), vwx40)
new_compare110(vwx30, vwx40, True, fc) → LT
new_primPlusNat0(Zero, vwx4100) → Succ(vwx4100)
new_lt4(vwx30, vwx40, eg, eh) → new_esEs9(new_compare6(vwx30, vwx40, eg, eh))
new_esEs14(vwx14, vwx15, ty_@0) → new_esEs8(vwx14, vwx15)
new_esEs19(Integer(vwx140), Integer(vwx150)) → new_primEqInt(vwx140, vwx150)
new_compare113(vwx30, vwx40, False) → GT
new_esEs26(vwx141, vwx151, app(ty_Ratio, cfe)) → new_esEs18(vwx141, vwx151, cfe)
new_compare8(vwx30, vwx40, ty_Double) → new_compare7(vwx30, vwx40)
new_esEs25(vwx140, vwx150, ty_Float) → new_esEs10(vwx140, vwx150)
new_not0True
new_esEs8(@0, @0) → True
new_compare28(vwx30, vwx40, True) → EQ
new_pePe(False, vwx14, vwx15, vwx31, beg) → new_asAs(new_esEs14(vwx14, vwx15, beg), vwx31)
new_compare8(vwx30, vwx40, ty_Bool) → new_compare17(vwx30, vwx40)
new_esEs27(vwx140, vwx150, ty_Int) → new_esEs11(vwx140, vwx150)
new_esEs14(vwx14, vwx15, ty_Bool) → new_esEs12(vwx14, vwx15)
new_esEs4(Right(vwx140), Right(vwx150), bfb, ty_Double) → new_esEs17(vwx140, vwx150)
new_primCmpInt(Pos(Succ(vwx300)), Neg(vwx40)) → GT
new_ltEs18(vwx31, vwx41, ty_Char) → new_ltEs7(vwx31, vwx41)
new_ltEs15(LT, EQ) → True
new_esEs14(vwx14, vwx15, app(app(ty_Either, bfb), bfc)) → new_esEs4(vwx14, vwx15, bfb, bfc)
new_primMulInt(Pos(vwx310), Pos(vwx410)) → Pos(new_primMulNat0(vwx310, vwx410))
new_primMulInt(Neg(vwx310), Neg(vwx410)) → Pos(new_primMulNat0(vwx310, vwx410))
new_lt11(vwx30, vwx40, app(ty_[], bcg)) → new_lt14(vwx30, vwx40, bcg)
new_esEs13(GT, GT) → True
new_primEqNat0(Zero, Succ(vwx1500)) → False
new_primEqNat0(Succ(vwx1400), Zero) → False
new_esEs5(Just(vwx140), Just(vwx150), app(ty_Ratio, ccd)) → new_esEs18(vwx140, vwx150, ccd)
new_esEs26(vwx141, vwx151, app(app(ty_@2, cff), cfg)) → new_esEs7(vwx141, vwx151, cff, cfg)
new_esEs14(vwx14, vwx15, ty_Double) → new_esEs17(vwx14, vwx15)
new_ltEs4(Right(vwx30), Right(vwx40), cc, ty_Integer) → new_ltEs11(vwx30, vwx40)
new_ltEs4(Right(vwx30), Right(vwx40), cc, app(ty_Ratio, dcc)) → new_ltEs16(vwx30, vwx40, dcc)
new_ltEs14(True, True) → True
new_ltEs19(vwx32, vwx42, ty_Char) → new_ltEs7(vwx32, vwx42)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_compare23(vwx30, vwx40, False, eg, eh) → new_compare10(vwx30, vwx40, new_ltEs4(vwx30, vwx40, eg, eh), eg, eh)
new_esEs27(vwx140, vwx150, app(app(ty_Either, cge), cgf)) → new_esEs4(vwx140, vwx150, cge, cgf)
new_esEs20(vwx142, vwx152, ty_Ordering) → new_esEs13(vwx142, vwx152)
new_compare111(vwx30, vwx40, False, fd, ff, fg) → GT
new_esEs27(vwx140, vwx150, app(app(app(ty_@3, chb), chc), chd)) → new_esEs6(vwx140, vwx150, chb, chc, chd)
new_compare4(:(vwx30, vwx31), [], baf) → GT
new_ltEs19(vwx32, vwx42, app(app(app(ty_@3, hh), baa), bab)) → new_ltEs8(vwx32, vwx42, hh, baa, bab)
new_ltEs6(Just(vwx30), Just(vwx40), app(ty_[], ed)) → new_ltEs9(vwx30, vwx40, ed)
new_esEs4(Left(vwx140), Left(vwx150), ty_Float, bfc) → new_esEs10(vwx140, vwx150)
new_lt20(vwx31, vwx41, ty_Float) → new_lt18(vwx31, vwx41)
new_esEs5(Just(vwx140), Just(vwx150), ty_Ordering) → new_esEs13(vwx140, vwx150)
new_esEs23(vwx141, vwx151, ty_Int) → new_esEs11(vwx141, vwx151)
new_lt20(vwx31, vwx41, ty_Ordering) → new_lt5(vwx31, vwx41)
new_compare8(vwx30, vwx40, ty_Ordering) → new_compare18(vwx30, vwx40)
new_esEs26(vwx141, vwx151, app(ty_Maybe, cfa)) → new_esEs5(vwx141, vwx151, cfa)
new_ltEs6(Just(vwx30), Just(vwx40), ty_Ordering) → new_ltEs15(vwx30, vwx40)
new_pePe(True, vwx14, vwx15, vwx31, beg) → True
new_ltEs7(vwx3, vwx4) → new_not(new_compare9(vwx3, vwx4))
new_esEs22(vwx140, vwx150, app(ty_[], cag)) → new_esEs15(vwx140, vwx150, cag)
new_primCmpInt(Neg(Zero), Neg(Succ(vwx400))) → new_primCmpNat0(Succ(vwx400), Zero)
new_compare23(vwx30, vwx40, True, eg, eh) → EQ
new_primCmpInt(Pos(Zero), Neg(Succ(vwx400))) → GT
new_compare110(vwx30, vwx40, False, fc) → GT
new_esEs5(Just(vwx140), Just(vwx150), app(app(app(ty_@3, ccg), cch), cda)) → new_esEs6(vwx140, vwx150, ccg, cch, cda)
new_compare4([], :(vwx40, vwx41), baf) → LT
new_ltEs4(Right(vwx30), Right(vwx40), cc, app(ty_[], dc)) → new_ltEs9(vwx30, vwx40, dc)
new_lt20(vwx31, vwx41, app(app(ty_@2, hc), hd)) → new_lt6(vwx31, vwx41, hc, hd)
new_esEs20(vwx142, vwx152, app(ty_Ratio, bgf)) → new_esEs18(vwx142, vwx152, bgf)
new_esEs15([], :(vwx150, vwx151), bfa) → False
new_esEs15(:(vwx140, vwx141), [], bfa) → False
new_esEs24(vwx140, vwx150, ty_Int) → new_esEs11(vwx140, vwx150)
new_ltEs19(vwx32, vwx42, ty_Integer) → new_ltEs11(vwx32, vwx42)
new_lt19(vwx30, vwx40, app(app(ty_Either, eg), eh)) → new_lt4(vwx30, vwx40, eg, eh)
new_lt11(vwx30, vwx40, ty_Int) → new_lt16(vwx30, vwx40)
new_primCmpInt(Neg(Zero), Neg(Zero)) → EQ
new_esEs25(vwx140, vwx150, ty_Bool) → new_esEs12(vwx140, vwx150)
new_compare8(vwx30, vwx40, app(ty_Maybe, bba)) → new_compare11(vwx30, vwx40, bba)
new_ltEs4(Right(vwx30), Right(vwx40), cc, app(app(ty_@2, dd), de)) → new_ltEs12(vwx30, vwx40, dd, de)
new_esEs20(vwx142, vwx152, app(ty_Maybe, bgb)) → new_esEs5(vwx142, vwx152, bgb)
new_lt20(vwx31, vwx41, app(ty_Maybe, gf)) → new_lt7(vwx31, vwx41, gf)
new_asAs(False, vwx40) → False
new_esEs18(:%(vwx140, vwx141), :%(vwx150, vwx151), bfd) → new_asAs(new_esEs24(vwx140, vwx150, bfd), new_esEs23(vwx141, vwx151, bfd))
new_lt11(vwx30, vwx40, ty_Double) → new_lt12(vwx30, vwx40)
new_primMulInt(Neg(vwx310), Pos(vwx410)) → Neg(new_primMulNat0(vwx310, vwx410))
new_primMulInt(Pos(vwx310), Neg(vwx410)) → Neg(new_primMulNat0(vwx310, vwx410))
new_esEs4(Right(vwx140), Right(vwx150), bfb, ty_Bool) → new_esEs12(vwx140, vwx150)
new_primMulNat0(Zero, Succ(vwx4100)) → Zero
new_primMulNat0(Succ(vwx3100), Zero) → Zero
new_compare16(vwx3, vwx4) → new_primCmpInt(vwx3, vwx4)
new_esEs13(GT, EQ) → False
new_esEs13(EQ, GT) → False
new_esEs15(:(vwx140, vwx141), :(vwx150, vwx151), bfa) → new_asAs(new_esEs25(vwx140, vwx150, bfa), new_esEs15(vwx141, vwx151, bfa))
new_lt20(vwx31, vwx41, app(ty_[], hb)) → new_lt14(vwx31, vwx41, hb)
new_compare4(:(vwx30, vwx31), :(vwx40, vwx41), baf) → new_primCompAux0(vwx30, vwx40, new_compare4(vwx31, vwx41, baf), baf)
new_ltEs19(vwx32, vwx42, ty_@0) → new_ltEs10(vwx32, vwx42)
new_not(EQ) → new_not0
new_esEs14(vwx14, vwx15, ty_Integer) → new_esEs19(vwx14, vwx15)
new_ltEs18(vwx31, vwx41, ty_Bool) → new_ltEs14(vwx31, vwx41)
new_compare13(@0, @0) → EQ
new_esEs4(Left(vwx140), Left(vwx150), app(ty_Maybe, chf), bfc) → new_esEs5(vwx140, vwx150, chf)
new_ltEs6(Just(vwx30), Just(vwx40), ty_Float) → new_ltEs17(vwx30, vwx40)
new_compare8(vwx30, vwx40, app(app(ty_@2, bbf), bbg)) → new_compare15(vwx30, vwx40, bbf, bbg)
new_esEs20(vwx142, vwx152, app(ty_[], bgc)) → new_esEs15(vwx142, vwx152, bgc)
new_esEs27(vwx140, vwx150, ty_Double) → new_esEs17(vwx140, vwx150)
new_esEs20(vwx142, vwx152, ty_Double) → new_esEs17(vwx142, vwx152)
new_esEs27(vwx140, vwx150, ty_Integer) → new_esEs19(vwx140, vwx150)
new_esEs25(vwx140, vwx150, app(app(app(ty_@3, ceb), cec), ced)) → new_esEs6(vwx140, vwx150, ceb, cec, ced)
new_esEs14(vwx14, vwx15, ty_Int) → new_esEs11(vwx14, vwx15)
new_esEs5(Just(vwx140), Just(vwx150), ty_@0) → new_esEs8(vwx140, vwx150)
new_ltEs4(Left(vwx30), Left(vwx40), ty_Double, bc) → new_ltEs5(vwx30, vwx40)
new_lt19(vwx30, vwx40, app(ty_[], fh)) → new_lt14(vwx30, vwx40, fh)
new_esEs25(vwx140, vwx150, ty_Integer) → new_esEs19(vwx140, vwx150)
new_esEs12(True, False) → False
new_esEs12(False, True) → False
new_ltEs12(@2(vwx30, vwx31), @2(vwx40, vwx41), bdb, bcb) → new_pePe(new_lt11(vwx30, vwx40, bdb), vwx30, vwx40, new_ltEs18(vwx31, vwx41, bcb), bdb)
new_esEs5(Nothing, Just(vwx150), beh) → False
new_esEs5(Just(vwx140), Nothing, beh) → False
new_ltEs4(Right(vwx30), Right(vwx40), cc, ty_Int) → new_ltEs13(vwx30, vwx40)
new_esEs26(vwx141, vwx151, app(ty_[], cfb)) → new_esEs15(vwx141, vwx151, cfb)
new_ltEs6(Nothing, Nothing, bee) → True
new_esEs20(vwx142, vwx152, ty_Integer) → new_esEs19(vwx142, vwx152)
new_esEs27(vwx140, vwx150, ty_Bool) → new_esEs12(vwx140, vwx150)
new_esEs5(Just(vwx140), Just(vwx150), ty_Integer) → new_esEs19(vwx140, vwx150)
new_ltEs4(Right(vwx30), Right(vwx40), cc, ty_Float) → new_ltEs17(vwx30, vwx40)
new_esEs4(Left(vwx140), Left(vwx150), app(app(ty_@2, dac), dad), bfc) → new_esEs7(vwx140, vwx150, dac, dad)
new_esEs14(vwx14, vwx15, ty_Float) → new_esEs10(vwx14, vwx15)
new_ltEs16(vwx3, vwx4, che) → new_not(new_compare19(vwx3, vwx4, che))
new_compare26(vwx30, vwx40, False) → new_compare113(vwx30, vwx40, new_ltEs14(vwx30, vwx40))
new_ltEs14(True, False) → False
new_ltEs17(vwx3, vwx4) → new_not(new_compare24(vwx3, vwx4))
new_esEs14(vwx14, vwx15, app(ty_[], bfa)) → new_esEs15(vwx14, vwx15, bfa)
new_esEs4(Right(vwx140), Right(vwx150), bfb, ty_Char) → new_esEs16(vwx140, vwx150)
new_not(LT) → new_not0
new_ltEs18(vwx31, vwx41, ty_Ordering) → new_ltEs15(vwx31, vwx41)
new_lt20(vwx31, vwx41, ty_Integer) → new_lt15(vwx31, vwx41)
new_esEs5(Nothing, Nothing, beh) → True
new_ltEs18(vwx31, vwx41, app(ty_Maybe, bde)) → new_ltEs6(vwx31, vwx41, bde)
new_esEs5(Just(vwx140), Just(vwx150), ty_Float) → new_esEs10(vwx140, vwx150)
new_compare112(vwx30, vwx40, False) → GT
new_ltEs6(Just(vwx30), Just(vwx40), ty_@0) → new_ltEs10(vwx30, vwx40)
new_lt19(vwx30, vwx40, ty_Double) → new_lt12(vwx30, vwx40)
new_compare8(vwx30, vwx40, app(ty_Ratio, bed)) → new_compare19(vwx30, vwx40, bed)
new_ltEs4(Left(vwx30), Left(vwx40), ty_Char, bc) → new_ltEs7(vwx30, vwx40)
new_lt19(vwx30, vwx40, ty_Float) → new_lt18(vwx30, vwx40)
new_compare27(vwx30, vwx40, True, fc) → EQ
new_compare27(vwx30, vwx40, False, fc) → new_compare110(vwx30, vwx40, new_ltEs6(vwx30, vwx40, fc), fc)
new_esEs22(vwx140, vwx150, ty_Float) → new_esEs10(vwx140, vwx150)
new_esEs20(vwx142, vwx152, app(app(ty_@2, bgg), bgh)) → new_esEs7(vwx142, vwx152, bgg, bgh)
new_esEs22(vwx140, vwx150, app(ty_Maybe, caf)) → new_esEs5(vwx140, vwx150, caf)
new_esEs21(vwx141, vwx151, app(ty_Maybe, bhd)) → new_esEs5(vwx141, vwx151, bhd)
new_primPlusNat1(Zero, Zero) → Zero
new_compare7(Double(vwx30, vwx31), Double(vwx40, vwx41)) → new_compare16(new_sr(vwx30, vwx40), new_sr(vwx31, vwx41))
new_ltEs4(Right(vwx30), Right(vwx40), cc, ty_Char) → new_ltEs7(vwx30, vwx40)
new_lt13(vwx30, vwx40) → new_esEs9(new_compare9(vwx30, vwx40))
new_esEs21(vwx141, vwx151, app(app(app(ty_@3, cac), cad), cae)) → new_esEs6(vwx141, vwx151, cac, cad, cae)
new_esEs26(vwx141, vwx151, app(app(ty_Either, cfc), cfd)) → new_esEs4(vwx141, vwx151, cfc, cfd)
new_ltEs4(Right(vwx30), Right(vwx40), cc, ty_Double) → new_ltEs5(vwx30, vwx40)
new_asAs(True, vwx40) → vwx40
new_ltEs15(GT, EQ) → False
new_esEs25(vwx140, vwx150, ty_Int) → new_esEs11(vwx140, vwx150)
new_primMulNat0(Succ(vwx3100), Succ(vwx4100)) → new_primPlusNat0(new_primMulNat0(vwx3100, Succ(vwx4100)), vwx4100)
new_lt9(vwx30, vwx40, fd, ff, fg) → new_esEs9(new_compare12(vwx30, vwx40, fd, ff, fg))
new_compare24(Float(vwx30, vwx31), Float(vwx40, vwx41)) → new_compare16(new_sr(vwx30, vwx40), new_sr(vwx31, vwx41))
new_ltEs4(Left(vwx30), Left(vwx40), ty_Integer, bc) → new_ltEs11(vwx30, vwx40)
new_esEs4(Left(vwx140), Right(vwx150), bfb, bfc) → False
new_esEs4(Right(vwx140), Left(vwx150), bfb, bfc) → False
new_esEs5(Just(vwx140), Just(vwx150), app(app(ty_@2, cce), ccf)) → new_esEs7(vwx140, vwx150, cce, ccf)
new_lt20(vwx31, vwx41, app(ty_Ratio, ceg)) → new_lt10(vwx31, vwx41, ceg)
new_lt20(vwx31, vwx41, ty_Bool) → new_lt17(vwx31, vwx41)
new_esEs4(Left(vwx140), Left(vwx150), app(app(app(ty_@3, dae), daf), dag), bfc) → new_esEs6(vwx140, vwx150, dae, daf, dag)
new_esEs27(vwx140, vwx150, ty_@0) → new_esEs8(vwx140, vwx150)
new_esEs25(vwx140, vwx150, ty_Ordering) → new_esEs13(vwx140, vwx150)
new_lt19(vwx30, vwx40, ty_Int) → new_lt16(vwx30, vwx40)
new_esEs26(vwx141, vwx151, ty_Char) → new_esEs16(vwx141, vwx151)
new_ltEs18(vwx31, vwx41, ty_Double) → new_ltEs5(vwx31, vwx41)
new_esEs4(Left(vwx140), Left(vwx150), ty_@0, bfc) → new_esEs8(vwx140, vwx150)
new_ltEs6(Just(vwx30), Just(vwx40), app(app(ty_@2, ee), ef)) → new_ltEs12(vwx30, vwx40, ee, ef)
new_ltEs6(Just(vwx30), Just(vwx40), app(ty_Ratio, bef)) → new_ltEs16(vwx30, vwx40, bef)
new_esEs20(vwx142, vwx152, ty_Char) → new_esEs16(vwx142, vwx152)
new_esEs21(vwx141, vwx151, ty_Bool) → new_esEs12(vwx141, vwx151)
new_primCompAux00(vwx45, GT) → GT
new_lt6(vwx30, vwx40, ga, gb) → new_esEs9(new_compare15(vwx30, vwx40, ga, gb))
new_esEs5(Just(vwx140), Just(vwx150), app(app(ty_Either, ccb), ccc)) → new_esEs4(vwx140, vwx150, ccb, ccc)
new_primCmpInt(Pos(Zero), Pos(Zero)) → EQ
new_esEs26(vwx141, vwx151, ty_Ordering) → new_esEs13(vwx141, vwx151)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs21(vwx141, vwx151, app(ty_Ratio, bhh)) → new_esEs18(vwx141, vwx151, bhh)
new_esEs4(Left(vwx140), Left(vwx150), app(ty_Ratio, dab), bfc) → new_esEs18(vwx140, vwx150, dab)
new_primCmpInt(Neg(Succ(vwx300)), Pos(vwx40)) → LT

The set Q consists of the following terms:

new_compare7(Double(x0, x1), Double(x2, x3))
new_lt20(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs27(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs7(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt20(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Zero, x0)
new_esEs25(x0, x1, ty_Float)
new_lt11(x0, x1, app(ty_[], x2))
new_ltEs8(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs20(x0, x1, ty_Ordering)
new_esEs4(Right(x0), Right(x1), x2, ty_Char)
new_lt11(x0, x1, app(ty_Maybe, x2))
new_esEs14(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_Double)
new_compare8(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Integer)
new_ltEs4(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs15(:(x0, x1), :(x2, x3), x4)
new_ltEs4(Right(x0), Right(x1), x2, ty_Double)
new_lt13(x0, x1)
new_esEs12(False, False)
new_esEs4(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs4(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs13(GT, GT)
new_esEs27(x0, x1, ty_Char)
new_ltEs4(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs14(x0, x1, ty_Integer)
new_esEs9(EQ)
new_lt20(x0, x1, app(ty_Ratio, x2))
new_compare23(x0, x1, True, x2, x3)
new_lt20(x0, x1, ty_@0)
new_ltEs18(x0, x1, ty_Float)
new_ltEs6(Just(x0), Just(x1), ty_Bool)
new_lt4(x0, x1, x2, x3)
new_esEs4(Right(x0), Right(x1), x2, ty_Ordering)
new_primCmpNat0(Succ(x0), Zero)
new_esEs4(Right(x0), Right(x1), x2, ty_@0)
new_ltEs7(x0, x1)
new_esEs5(Just(x0), Nothing, x1)
new_ltEs19(x0, x1, app(app(ty_@2, x2), x3))
new_compare112(x0, x1, True)
new_lt11(x0, x1, ty_Ordering)
new_ltEs14(True, False)
new_ltEs14(False, True)
new_esEs27(x0, x1, ty_Bool)
new_ltEs19(x0, x1, app(ty_Maybe, x2))
new_lt19(x0, x1, ty_Char)
new_primCmpInt(Neg(Succ(x0)), Neg(x1))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare26(x0, x1, True)
new_esEs4(Right(x0), Right(x1), x2, ty_Bool)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_primMulInt(Neg(x0), Neg(x1))
new_ltEs18(x0, x1, app(ty_Ratio, x2))
new_esEs4(Left(x0), Left(x1), ty_Bool, x2)
new_ltEs18(x0, x1, app(ty_[], x2))
new_esEs8(@0, @0)
new_primCmpNat0(Succ(x0), Succ(x1))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs18(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Integer)
new_esEs4(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_compare8(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs11(x0, x1)
new_compare18(x0, x1)
new_esEs15([], [], x0)
new_ltEs19(x0, x1, ty_Double)
new_primCompAux0(x0, x1, x2, x3)
new_ltEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_lt11(x0, x1, ty_Float)
new_esEs4(Right(x0), Right(x1), x2, ty_Double)
new_lt11(x0, x1, ty_Int)
new_primMulNat0(Succ(x0), Zero)
new_compare26(x0, x1, False)
new_esEs20(x0, x1, ty_Bool)
new_primCmpNat0(Zero, Succ(x0))
new_ltEs4(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs4(Left(x0), Left(x1), ty_Int, x2)
new_esEs14(x0, x1, app(ty_[], x2))
new_lt16(x0, x1)
new_esEs14(x0, x1, ty_Char)
new_ltEs4(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_ltEs4(Left(x0), Left(x1), ty_Float, x2)
new_esEs14(x0, x1, app(app(ty_@2, x2), x3))
new_esEs13(GT, LT)
new_esEs13(LT, GT)
new_lt19(x0, x1, ty_Float)
new_lt19(x0, x1, app(ty_Maybe, x2))
new_ltEs6(Just(x0), Just(x1), ty_Ordering)
new_compare8(x0, x1, app(ty_Maybe, x2))
new_pePe(True, x0, x1, x2, x3)
new_lt20(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Int)
new_ltEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Zero)
new_lt19(x0, x1, ty_Integer)
new_compare28(x0, x1, False)
new_esEs14(x0, x1, ty_Ordering)
new_primCompAux00(x0, LT)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs4(Left(x0), Left(x1), ty_@0, x2)
new_esEs27(x0, x1, ty_Double)
new_lt11(x0, x1, ty_@0)
new_esEs4(Left(x0), Left(x1), ty_Float, x2)
new_ltEs6(Nothing, Nothing, x0)
new_ltEs19(x0, x1, app(ty_[], x2))
new_esEs13(EQ, GT)
new_esEs13(GT, EQ)
new_lt15(x0, x1)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_lt20(x0, x1, ty_Float)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs19(x0, x1, app(ty_Ratio, x2))
new_compare8(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, ty_Float)
new_pePe(False, x0, x1, x2, x3)
new_primMulNat0(Zero, Zero)
new_lt20(x0, x1, ty_Char)
new_ltEs4(Left(x0), Left(x1), ty_Char, x2)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_compare8(x0, x1, ty_Double)
new_esEs24(x0, x1, ty_Integer)
new_esEs5(Just(x0), Just(x1), ty_Int)
new_compare8(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare8(x0, x1, ty_Ordering)
new_lt11(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs16(x0, x1, x2)
new_esEs22(x0, x1, ty_Int)
new_esEs25(x0, x1, ty_@0)
new_ltEs18(x0, x1, ty_@0)
new_ltEs6(Just(x0), Just(x1), ty_Char)
new_ltEs18(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_Ordering)
new_compare8(x0, x1, ty_Integer)
new_compare111(x0, x1, True, x2, x3, x4)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_compare8(x0, x1, ty_@0)
new_ltEs17(x0, x1)
new_esEs25(x0, x1, ty_Ordering)
new_esEs15(:(x0, x1), [], x2)
new_esEs5(Just(x0), Just(x1), ty_Double)
new_esEs4(Right(x0), Right(x1), x2, ty_Int)
new_esEs13(EQ, EQ)
new_ltEs15(GT, EQ)
new_ltEs15(EQ, GT)
new_esEs5(Just(x0), Just(x1), ty_Bool)
new_esEs20(x0, x1, ty_@0)
new_lt20(x0, x1, ty_Double)
new_ltEs19(x0, x1, ty_Ordering)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs19(Integer(x0), Integer(x1))
new_primCmpInt(Neg(Zero), Neg(Succ(x0)))
new_esEs26(x0, x1, ty_Char)
new_ltEs12(@2(x0, x1), @2(x2, x3), x4, x5)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs20(x0, x1, ty_Integer)
new_compare111(x0, x1, False, x2, x3, x4)
new_esEs4(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_lt11(x0, x1, ty_Double)
new_lt14(x0, x1, x2)
new_compare28(x0, x1, True)
new_asAs(True, x0)
new_ltEs4(Right(x0), Right(x1), x2, ty_Char)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_compare19(:%(x0, x1), :%(x2, x3), ty_Int)
new_ltEs19(x0, x1, ty_Char)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_ltEs6(Nothing, Just(x0), x1)
new_compare29(x0, x1, False, x2, x3)
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Double)
new_esEs4(Left(x0), Left(x1), ty_Double, x2)
new_compare4(:(x0, x1), [], x2)
new_compare113(x0, x1, False)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs5(Just(x0), Just(x1), ty_Ordering)
new_ltEs15(LT, GT)
new_ltEs15(GT, LT)
new_primCmpInt(Neg(Zero), Pos(Succ(x0)))
new_primCmpInt(Pos(Zero), Neg(Succ(x0)))
new_esEs22(x0, x1, app(ty_[], x2))
new_ltEs15(GT, GT)
new_compare114(x0, x1, False, x2, x3)
new_lt19(x0, x1, ty_Double)
new_esEs4(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs11(x0, x1)
new_primPlusNat1(Zero, Zero)
new_not0
new_primMulInt(Pos(x0), Neg(x1))
new_primMulInt(Neg(x0), Pos(x1))
new_compare29(x0, x1, True, x2, x3)
new_esEs5(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_Char)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs14(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs9(GT)
new_esEs27(x0, x1, ty_Ordering)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_ltEs4(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs25(x0, x1, ty_Int)
new_lt9(x0, x1, x2, x3, x4)
new_ltEs6(Just(x0), Just(x1), ty_Integer)
new_compare27(x0, x1, True, x2)
new_compare12(x0, x1, x2, x3, x4)
new_primEqNat0(Succ(x0), Zero)
new_ltEs13(x0, x1)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_lt19(x0, x1, ty_@0)
new_primCmpInt(Neg(Zero), Neg(Zero))
new_lt17(x0, x1)
new_ltEs4(Left(x0), Right(x1), x2, x3)
new_ltEs4(Right(x0), Left(x1), x2, x3)
new_ltEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt20(x0, x1, ty_Ordering)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_compare4([], [], x0)
new_esEs4(Right(x0), Right(x1), x2, ty_Integer)
new_ltEs15(LT, LT)
new_primEqNat0(Succ(x0), Succ(x1))
new_ltEs4(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs10(Float(x0, x1), Float(x2, x3))
new_ltEs6(Just(x0), Just(x1), ty_Double)
new_esEs4(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_primPlusNat1(Succ(x0), Succ(x1))
new_ltEs19(x0, x1, ty_@0)
new_ltEs4(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_lt7(x0, x1, x2)
new_not(GT)
new_esEs12(True, True)
new_ltEs18(x0, x1, app(ty_Maybe, x2))
new_lt20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt18(x0, x1)
new_primMulNat0(Zero, Succ(x0))
new_esEs16(Char(x0), Char(x1))
new_esEs25(x0, x1, ty_Integer)
new_esEs4(Right(x0), Right(x1), x2, app(ty_[], x3))
new_compare25(x0, x1, True, x2, x3, x4)
new_esEs20(x0, x1, ty_Float)
new_lt11(x0, x1, ty_Char)
new_esEs17(Double(x0, x1), Double(x2, x3))
new_compare4(:(x0, x1), :(x2, x3), x4)
new_esEs6(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_lt11(x0, x1, ty_Bool)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_lt8(x0, x1)
new_sr(x0, x1)
new_compare13(@0, @0)
new_lt10(x0, x1, x2)
new_esEs4(Left(x0), Right(x1), x2, x3)
new_esEs4(Right(x0), Left(x1), x2, x3)
new_compare8(x0, x1, app(ty_[], x2))
new_compare15(x0, x1, x2, x3)
new_ltEs4(Left(x0), Left(x1), app(ty_[], x2), x3)
new_primCmpInt(Pos(Zero), Pos(Zero))
new_lt11(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt20(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs4(Left(x0), Left(x1), ty_Integer, x2)
new_ltEs18(x0, x1, ty_Int)
new_compare110(x0, x1, True, x2)
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, ty_Int)
new_ltEs19(x0, x1, ty_Integer)
new_esEs4(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_compare8(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Double)
new_lt19(x0, x1, app(ty_[], x2))
new_sr0(Integer(x0), Integer(x1))
new_esEs4(Right(x0), Right(x1), x2, ty_Float)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_primCmpInt(Pos(Zero), Pos(Succ(x0)))
new_compare16(x0, x1)
new_esEs22(x0, x1, ty_Float)
new_esEs21(x0, x1, ty_@0)
new_ltEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs4(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs27(x0, x1, ty_@0)
new_esEs26(x0, x1, ty_@0)
new_esEs21(x0, x1, ty_Double)
new_lt11(x0, x1, app(ty_Ratio, x2))
new_esEs5(Just(x0), Just(x1), ty_Char)
new_esEs5(Just(x0), Just(x1), ty_@0)
new_lt5(x0, x1)
new_esEs20(x0, x1, ty_Char)
new_primEqNat0(Zero, Succ(x0))
new_compare23(x0, x1, False, x2, x3)
new_ltEs4(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs5(Nothing, Just(x0), x1)
new_ltEs9(x0, x1, x2)
new_esEs4(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs9(LT)
new_compare10(x0, x1, True, x2, x3)
new_compare112(x0, x1, False)
new_esEs20(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Int)
new_ltEs4(Left(x0), Left(x1), ty_Int, x2)
new_compare17(x0, x1)
new_primCmpInt(Pos(Succ(x0)), Pos(x1))
new_esEs4(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_ltEs4(Right(x0), Right(x1), x2, ty_Ordering)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_ltEs19(x0, x1, app(app(ty_Either, x2), x3))
new_compare14(Integer(x0), Integer(x1))
new_lt12(x0, x1)
new_primCmpNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), x1)
new_ltEs4(Right(x0), Right(x1), x2, ty_@0)
new_compare113(x0, x1, True)
new_ltEs18(x0, x1, ty_Bool)
new_ltEs6(Just(x0), Just(x1), ty_@0)
new_esEs21(x0, x1, ty_Char)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat1(Zero, Succ(x0))
new_ltEs6(Just(x0), Just(x1), ty_Float)
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_compare4([], :(x0, x1), x2)
new_esEs22(x0, x1, ty_Integer)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_ltEs19(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Bool)
new_esEs5(Nothing, Nothing, x0)
new_lt19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(LT, LT)
new_esEs21(x0, x1, app(ty_[], x2))
new_lt20(x0, x1, app(ty_[], x2))
new_ltEs4(Right(x0), Right(x1), x2, ty_Float)
new_ltEs4(Right(x0), Right(x1), x2, ty_Bool)
new_esEs4(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_lt19(x0, x1, app(app(ty_Either, x2), x3))
new_compare27(x0, x1, False, x2)
new_esEs12(False, True)
new_esEs12(True, False)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_ltEs14(True, True)
new_ltEs14(False, False)
new_esEs5(Just(x0), Just(x1), ty_Integer)
new_ltEs4(Left(x0), Left(x1), ty_@0, x2)
new_esEs25(x0, x1, app(ty_[], x2))
new_ltEs6(Just(x0), Just(x1), app(ty_[], x2))
new_ltEs18(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Char)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs5(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs14(x0, x1, ty_@0)
new_compare9(Char(x0), Char(x1))
new_lt20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, ty_Bool)
new_esEs21(x0, x1, ty_Int)
new_esEs5(Just(x0), Just(x1), ty_Float)
new_esEs21(x0, x1, ty_Bool)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_not(EQ)
new_esEs26(x0, x1, ty_Ordering)
new_esEs13(LT, EQ)
new_esEs13(EQ, LT)
new_lt19(x0, x1, app(ty_Ratio, x2))
new_primCompAux00(x0, GT)
new_compare11(x0, x1, x2)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs14(x0, x1, app(ty_Maybe, x2))
new_ltEs18(x0, x1, ty_Double)
new_primCmpInt(Neg(Zero), Pos(Zero))
new_primCmpInt(Pos(Zero), Neg(Zero))
new_ltEs4(Left(x0), Left(x1), ty_Integer, x2)
new_esEs14(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_compare24(Float(x0, x1), Float(x2, x3))
new_compare10(x0, x1, False, x2, x3)
new_ltEs19(x0, x1, ty_Bool)
new_ltEs4(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_asAs(False, x0)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_compare8(x0, x1, ty_Float)
new_ltEs18(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(Left(x0), Left(x1), ty_Char, x2)
new_ltEs6(Just(x0), Nothing, x1)
new_primCmpInt(Neg(Succ(x0)), Pos(x1))
new_ltEs6(Just(x0), Just(x1), ty_Int)
new_primCmpInt(Pos(Succ(x0)), Neg(x1))
new_ltEs15(EQ, LT)
new_ltEs15(LT, EQ)
new_esEs5(Just(x0), Just(x1), app(ty_[], x2))
new_lt19(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Float)
new_esEs27(x0, x1, ty_Int)
new_esEs14(x0, x1, ty_Int)
new_primMulInt(Pos(x0), Pos(x1))
new_ltEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs19(x0, x1, ty_Int)
new_ltEs4(Right(x0), Right(x1), x2, ty_Integer)
new_compare8(x0, x1, ty_Int)
new_esEs14(x0, x1, ty_Bool)
new_ltEs15(EQ, EQ)
new_compare6(x0, x1, x2, x3)
new_ltEs4(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_compare8(x0, x1, ty_Bool)
new_lt20(x0, x1, ty_Int)
new_ltEs18(x0, x1, app(app(ty_Either, x2), x3))
new_compare110(x0, x1, False, x2)
new_primPlusNat1(Succ(x0), Zero)
new_esEs14(x0, x1, app(ty_Ratio, x2))
new_lt19(x0, x1, ty_Ordering)
new_esEs20(x0, x1, app(ty_[], x2))
new_ltEs4(Left(x0), Left(x1), ty_Double, x2)
new_esEs4(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_ltEs10(x0, x1)
new_compare19(:%(x0, x1), :%(x2, x3), ty_Integer)
new_compare114(x0, x1, True, x2, x3)
new_ltEs4(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_lt11(x0, x1, ty_Integer)
new_ltEs18(x0, x1, ty_Char)
new_esEs5(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_Float)
new_ltEs4(Left(x0), Left(x1), ty_Bool, x2)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_lt19(x0, x1, ty_Bool)
new_esEs15([], :(x0, x1), x2)
new_esEs25(x0, x1, ty_Bool)
new_ltEs4(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs14(x0, x1, ty_Double)
new_ltEs5(x0, x1)
new_lt6(x0, x1, x2, x3)
new_esEs5(Just(x0), Just(x1), app(ty_Maybe, x2))
new_compare25(x0, x1, False, x2, x3, x4)
new_not(LT)
new_esEs22(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_@0)
new_lt19(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs4(Right(x0), Right(x1), x2, ty_Int)
new_lt11(x0, x1, app(app(ty_@2, x2), x3))
new_primCompAux00(x0, EQ)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: